T:Type, X:MaInterface(T), es:ES, e:E. ma-in-interface(es;X;e)   

latex

Definitions

t  T, x:A. B(x), x. t(x), Knd, Type, Id, a:A fp B(a), b, {x:A| B(x)} , State(ds), Top, left + right, x:AB(x), x:A  B(x), f(x), t.1, t.2, kind(e), P  Q, , s = t, A, P & Q, P  Q, Unit, E, ES, ma-in-interface(es;X;e), MaInterface(T), loc(e), IdDeq, x  dom(f), if b then t else f fi , strong-subtype(A;B), , x.A(x), EqDecider(T), KindDeq, tt, ff, b, IdLnk, False, True, case b of inl(x) => s(x) | inr(y) => t(y), hasloc(k;i)

Lemmas

es-kind wf, true wf, false wf, bnot wf, bfalse wf, btrue wf, es-hasloc, Kind-deq wf, hasloc wf, decl-state wf, pi1 wf, fpf-ap wf, fpf wf, top wf, strong-subtype-deq-subtype, strong-subtype-set3, assert wf, strong-subtype-self, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, pi2 wf, fpf-trivial-subtype-top